AXIOM TRANS
(∀ X) (∀ Y) (∀ Z) (X=Y∧Y=Z⊃X=Z) 

AXIOM SYM
(∀ X) (∀ Y) (X=Y⊃Y=X) 

AXIOM REFLEX
(∀ X) (X=X) 

AXIOM BIGINTER
(∀ X) (ISSET X∧(∀ Y) (YεX⊃ISSET Y)⊃ISSET BIGINTER X∧(∀ Z) (Zε
BIGUNION X≡(∀ Y) (YεX⊃ZεY))) 

AXIOM BIGUNION
(∀ X) (ISSET X∧(∀ Y) (YεX⊃ISSET Y)⊃ISSET BIGUNION X∧(∀ Z) (Zε
BIGUNION X≡(∃ Y) (YεX∧ZεY))) 

AXIOM DIFFSET
(∀ X) (∀ Y) (ISSET X∧ISSET Y⊃ISSET (X-Y)∧(∀ Z) (ZεX-Y≡ZεX∧¬ (ZεY))) 

AXIOM FNDEF
(∀ FF) (∀ U) (∀ V) (ISSET U∧ISSET V∧ISSET FF∧FFCONTAINEDUPRODUCTV∧(∀ 
X) (XεU⊃(∃ Y) (YεV∧X.YεFF))∧(∀ X) (∀ Y) (∀ Z) (XεU∧YεV∧X.YεFF∧X.ZεFF
⊃Y=Z)⊃(∃ F) (FεU → V∧(∀ X) (XεU⊃X.α(F,X)εFF))) 

AXIOM EQFN
(∀ U) (∀ V) (∀ F) (∀ G) (FεU → V∧GεU → V⊃(F=G≡(∀ X) (XεU⊃α(F,X)=α(G
,X)))) 

AXIOM APPLY
(∀ F) (∀ X) (∀ U) (∀ V) (FεU → V∧XεU⊃α(F,X)εV) 

AXIOM POWERSET
(∀ X) (∀ Y) (ISSET X∧ISSET Y⊃ISSET X → Y) 

AXIOM CONTAIN
(∀ U) (∀ V) (UCONTAINEDV≡(∀ X) (XεU⊃XεV)) 

AXIOM PAIR
(∀ X) (∀ Y) (∀ U) (∀ V) (X.Y=U.V≡X=U∧Y=V) 

AXIOM CARTESIAN
(∀ X) (∀ Y) (∀ Z) (ZεXPRODUCTY≡(∃ U) (∃ V) (UεX∧VεY∧Z=U.V)) 

AXIOM CARTSET
(∀ X) (∀ Y) (ISSET X∧ISSET Y⊃ISSET (XPRODUCTY)) 

AXIOM INTER
(∀ X) (∀ Y) (∀ Z) (ZεXINTERSECTIONY≡ZεX∨ZεY) 

AXIOM INTERSET
(∀ X) (∀ Y) (ISSET X∧ISSET Y⊃ISSET (XINTERSECTIONY)) 

AXIOM UNIONAX
(∀ X) (∀ Y) (∀ Z) (ZεXUNIONY≡ZεX∨ZεY) 

AXIOM UNIONSET
(∀ X) (∀ Y) (ISSET X∧ISSET Y⊃ISSET (XUNIONY)) 

AXIOM UNITSET
(∀ X) (∀ Y) (YεUNITSET X≡Y=X) 

AXIOM NULL1
(∀ X) ¬ (XεNULLSET) 

AXIOM NULLSET
ISSET NULLSET 

AXIOM EXTENSIONALITY
(∀ U) (∀ V) (ISSET U∧ISSET V⊃(∀ X) (XεU≡XεV)⊃U=V) 

AXIOM PLUSS
(∀ X) (∀ Y) (XεI0∧YεI0⊃(Y=0⊃X+Y=X)∧(¬ (Y=0)⊃X+Y=SUCC X+PRED Y)) 

AXIOM INDUCTION
(∀ U) (UCONTAINEDI0∧0εU∧(∀ X) (XεU⊃SUCC XεU)⊃U=I0) 

AXIOM SP
(∀ X) (XεI0∧¬ (X=0)⊃X=SUCC PRED X) 

AXIOM PS
(∀ X) (XεI0⊃X=PRED SUCC X) 

AXIOM SN0
(∀ X) (XεI0⊃¬ (SUCC X=0)) 

AXIOM PRED
(∀ X) (XεI0∧¬ (X=0)⊃PRED XεI0) 

AXIOM INT0
0εI0 

AXIOM SUCC
(∀ X) (XεI0⊃SUCC XεI0) 

AXIOM INTSET
ISSET I0 

SCHEMA COMPREHENSION
(PRED PP) (∀ UU) (ISSET UU⊃(∃ WW) (ISSET WW∧(∀ XX) (XXεWW≡XXεUU∧PP 
XX))) 

PROOF ONE 

1:	(∀ UU) (ISSET UU⊃(∃ WW) (ISSET WW∧(∀ XX) (XXεWW≡XXεUU∧(∀ X) (
XεI0⊃SUCC X+XX=SUCC (X+XX))))) BY SCHEMA(COMPREHENSION,(λ Y) (∀ X) (
XεI0⊃SUCC X+Y=SUCC (X+Y))) 

2:	ISSET I0⊃(∃ WW) (ISSET WW∧(∀ XX) (XXεWW≡XXεI0∧(∀ X) (XεI0⊃
SUCC X+XX=SUCC (X+XX)))) BY US(1,I0) 

3:	ISSET I0 BY AXIOM INTSET 

4:	(∃ WW) (ISSET WW∧(∀ XX) (XXεWW≡XXεI0∧(∀ X) (XεI0⊃SUCC X+XX=
SUCC (X+XX)))) BY MP(2,3) 

5:	ISSET A∧(∀ XX) (XXεA≡XXεI0∧(∀ X) (XεI0⊃SUCC X+XX=SUCC (X+XX))~
) BY US(4,A) 

6:	ISSET A BY AE(5,1) 

7:	(∀ XX) (XXεA≡XXεI0∧(∀ X) (XεI0⊃SUCC X+XX=SUCC (X+XX))) BY AE(
5,2) 

8:	0εA≡0εI0∧(∀ X) (XεI0⊃SUCC X+0=SUCC (X+0)) BY US(7,0) 

9:	0εI0 BY AXIOM INT0 

10:	0=0 BY AXIOM(REFLEX,0) 

11:	XεI0∧0εI0⊃(0=0⊃X+0=X)∧(¬ (0=0)⊃X+0=SUCC X+PRED 0) BY AXIOM(
PLUSS,X,0) 

12:	XεI0⊃X+0=X BY TAUT(XεI0⊃X+0=X,9,10,11) 

13:	(∀ X) (XεI0⊃X+0=X) BY UG(12,X) 

14:	XεI0 BY ASSUMPTION 

15:	X+0=X BY MP(12,14) ASSUMING (14) 

16:	SUCC X=SUCC X BY AXIOM(REFLEX,SUCC X) 

17:	SUCC X=SUCC (X+0) BY REPR(16,15,2) ASSUMING (14) 

18:	SUCC XεI0⊃SUCC X+0=SUCC X BY THEOREM(P0,SUCC X) 

19:	SUCC X+0=SUCC X∧SUCC X=SUCC (X+0)⊃SUCC X+0=SUCC (X+0) BY 
AXIOM(TRANS,SUCC X+0,SUCC X,SUCC (X+0)) 

20:	XεI0⊃SUCC X=SUCC (X+0) BY DED(17,14) 

21:	XεI0⊃SUCC XεI0 BY AXIOM(SUCC,X) 

22:	XεI0⊃SUCC X+0=SUCC (X+0) BY TAUT(XεI0⊃SUCC X+0=SUCC (X+0),21
,20,19,18) 

23:	(∀ X) (XεI0⊃SUCC X+0=SUCC (X+0)) BY UG(22,X) 

24:	0εA BY TAUT(0εA,9,8,23) 

25:	YεA BY ASSUMPTION 

26:	YεA≡YεI0∧(∀ X) (XεI0⊃SUCC X+Y=SUCC (X+Y)) BY US(7,Y) 

27:	(∀ X) (XεI0⊃SUCC X+Y=SUCC (X+Y)) BY TAUT((∀ X) (XεI0⊃SUCC X
+Y=SUCC (X+Y)),25,26) ASSUMING (25) 

28:	SUCC XεI0⊃SUCC SUCC X+Y=SUCC (SUCC X+Y) BY US(27,SUCC X) ASSU~
MING (25) 

29:	SUCC XεI0∧SUCC YεI0⊃(SUCC Y=0⊃SUCC X+SUCC Y=SUCC X)∧(¬ (SUCC 
Y=0)⊃SUCC X+SUCC Y=SUCC SUCC X+PRED SUCC Y) BY AXIOM(PLUSS,SUCC X,
SUCC Y) 

30:	YεI0⊃SUCC YεI0 BY AXIOM(SUCC,Y) 

31:	SUCC YεI0 BY TAUT(SUCC YεI0,30,25,26) ASSUMING (25) 

32:	YεI0⊃¬ (SUCC Y=0) BY AXIOM(SN0,Y) 

33:	YεI0 BY TAUT(YεI0,25,26) ASSUMING (25) 

34:	XεI0⊃SUCC X+SUCC Y=SUCC SUCC X+PRED SUCC Y BY TAUT(XεI0⊃SUCC 
X+SUCC Y=SUCC SUCC X+PRED SUCC Y,29,33,30,32,21) ASSUMING (25) 

35:	YεI0⊃Y=PRED SUCC Y BY AXIOM(PS,Y) 

36:	Y=PRED SUCC Y BY MP(35,33) ASSUMING (25) 

37:	XεI0⊃SUCC X+SUCC Y=SUCC SUCC X+Y BY REPR(34,36,1) ASSUMING (2~
5) 

38:	XεI0∧SUCC YεI0⊃(SUCC Y=0⊃X+SUCC Y=X)∧(¬ (SUCC Y=0)⊃X+SUCC Y=
SUCC X+PRED SUCC Y) BY AXIOM(PLUSS,X,SUCC Y) 

39:	XεI0⊃X+SUCC Y=SUCC X+PRED SUCC Y BY TAUT(XεI0⊃X+SUCC Y=SUCC 
X+PRED SUCC Y,38,33,31,32) ASSUMING (25) 

40:	XεI0⊃X+SUCC Y=SUCC X+Y BY REPR(39,36,1) ASSUMING (25) 

41:	X+SUCC Y=SUCC X+Y BY MP(14,40) ASSUMING (14 25) 

42:	SUCC (X+SUCC Y)=SUCC (X+SUCC Y) BY AXIOM(REFLEX,SUCC (X+SUCC 
Y)) 

43:	SUCC (X+SUCC Y)=SUCC (SUCC X+Y) BY REPL(42,41,2) ASSUMING (14~
 25) 

44:	XεI0⊃SUCC (X+SUCC Y)=SUCC (SUCC X+Y) BY DED(43,14) ASSUMING (~
25) 

45:	SUCC XεI0 BY MP(14,21) ASSUMING (14) 

46:	SUCC SUCC X+Y=SUCC (SUCC X+Y) BY MP(45,28) ASSUMING (14 25) 

47:	SUCC X+SUCC Y=SUCC SUCC X+Y BY MP(14,37) ASSUMING (14 25) 

48:	SUCC (X+SUCC Y)=SUCC (SUCC X+Y) BY MP(14,44) ASSUMING (14 25)~
 

49:	SUCC X+SUCC Y=SUCC X+SUCC Y BY AXIOM(REFLEX,SUCC X+SUCC Y) 

50:	SUCC X+SUCC Y=SUCC SUCC X+Y BY REPL(49,47,2) ASSUMING (14 25)~
 

51:	SUCC X+SUCC Y=SUCC (SUCC X+Y) BY REPL(50,46,1) ASSUMING (14 2~
5) 

52:	SUCC X+SUCC Y=SUCC (X+SUCC Y) BY REPR(51,48,1) ASSUMING (14 2~
5) 

53:	XεI0⊃SUCC X+SUCC Y=SUCC (X+SUCC Y) BY DED(52,14) ASSUMING (25~
) 

54:	(∀ X) (XεI0⊃SUCC X+SUCC Y=SUCC (X+SUCC Y)) BY UG(53,X) ASSUMI~
NG (25) 

55:	SUCC YεI0∧(∀ X) (XεI0⊃SUCC X+SUCC Y=SUCC (X+SUCC Y)) BY AI(
31,54) ASSUMING (25) 

56:	SUCC YεA≡SUCC YεI0∧(∀ X) (XεI0⊃SUCC X+SUCC Y=SUCC (X+SUCC Y))~
 BY US(7,SUCC Y) 

57:	SUCC YεA BY TAUT(SUCC YεA,56,55) ASSUMING (25) 

58:	YεA⊃SUCC YεA BY DED(57,25) 

59:	(∀ Y) (YεA⊃SUCC YεA) BY UG(58,Y) 

60:	XεA⊃SUCC XεA BY US(59,X) 

61:	(∀ X) (XεA⊃SUCC XεA) BY UG(60,X) 

62:	ACONTAINEDI0≡(∀ X) (XεA⊃XεI0) BY AXIOM(CONTAIN,A,I0) 

63:	YεA⊃YεI0 BY TAUT(YεA⊃YεI0,26) 

64:	(∀ Y) (YεA⊃YεI0) BY UG(63,Y) 

65:	XεA⊃XεI0 BY US(64,X) 

66:	(∀ X) (XεA⊃XεI0) BY UG(65,X) 

67:	ACONTAINEDI0 BY TAUT(ACONTAINEDI0,62,66) 

68:	ACONTAINEDI0∧0εA∧(∀ X) (XεA⊃SUCC XεA)⊃A=I0 BY AXIOM(
INDUCTION,A) 

69:	A=I0 BY TAUT(A=I0,68,67,24,61) 

70:	YεI0≡YεI0∧(∀ X) (XεI0⊃SUCC X+Y=SUCC (X+Y)) BY REPL(26,69,1) 

71:	YεI0⊃(∀ X) (XεI0⊃SUCC X+Y=SUCC (X+Y)) BY TAUT(YεI0⊃(∀ X) (Xε
I0⊃SUCC X+Y=SUCC (X+Y)),70) 

72:	YεI0 BY ASSUMPTION 

73:	(∀ X) (XεI0⊃SUCC X+Y=SUCC (X+Y)) BY MP(72,71) ASSUMING (72) 

74:	XεI0⊃SUCC X+Y=SUCC (X+Y) BY US(73,X) ASSUMING (72) 

75:	YεI0⊃XεI0⊃SUCC X+Y=SUCC (X+Y) BY DED(74,72) 

76:	XεI0∧YεI0⊃SUCC X+Y=SUCC (X+Y) BY TAUT(XεI0∧YεI0⊃SUCC X+Y=
SUCC (X+Y),75) 

77:	(∀ X) (∀ Y) (XεI0∧YεI0⊃SUCC X+Y=SUCC (X+Y)) BY UG(76,Y,X) 

THEOREM P0 
(∀ X) (XεI0⊃X+0=X) 
THEOREM TH1 
(∀ X) (∀ Y) (XεI0∧YεI0⊃SUCC X+Y=SUCC (X+Y))